// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_MATH_POSITIONAL
#define _sHT_MATH_POSITIONAL

#include <sHT/math/expnat.h>
#include <sHT/math/expnat/lt.h>
#include <sHT/math/vector.h>

/*@ axiomatic Positional {
      // v: most-significant to least-significant digit values
      // b: radix
      logic ℤ sum_digits_ms_to_ls(ℤ b, \list<ℤ> v)
        = sum(cross(v, exp_countdown(b, \length(v))));

      lemma sum_digits_ms_to_ls_empty: ∀ ℤ b;
        sum_digits_ms_to_ls(b, [| |]) == 0;

      lemma sum_digits_ms_to_ls_ind: ∀ ℤ b, d, \list<ℤ> v;
        sum_digits_ms_to_ls(b, v ^ [| d |])
        == b * sum_digits_ms_to_ls(b, v) + d;
    } */

/*@ axiomatic PositionalBounds {
      lemma sum_digits_lt_base: ∀ ℤ a;
        1 < a ==> sum_digits_ms_to_ls(a, [| |]) < 1;

      lemma sum_digits_lt_ind: ∀ ℤ a, \list<ℤ> v, ℤ b;
        1 < a && vector_lt_constant(v ^ [| b |], a)
        && sum_digits_ms_to_ls(a, v) < expnat(a, \length(v))
        ==> sum_digits_ms_to_ls(a, v ^ [| b |]) < expnat(a, \length(v) + 1);

      // Proof: induction: sum_digits_lt_base and sum_digits_lt_ind
      lemma sum_digits_lt: ∀ ℤ a, \list<ℤ> v;
        1 < a && vector_lt_constant(v, a)
        ==> sum_digits_ms_to_ls(a, v) < expnat(a, \length(v));
    } */

/*@ axiomatic PositionalPositive {
      lemma sum_digits_positive_0: ∀ ℤ a;
        0 ≤ a ⇒ 0 ≤ sum_digits_ms_to_ls(a, [| |]);

      lemma sum_digits_positive_S: ∀ ℤ a, \list<ℤ> v, ℤ d;
        0 ≤ a ∧ 0 ≤ d ∧ 0 ≤ sum_digits_ms_to_ls(a, v)
        ⇒ 0 ≤ sum_digits_ms_to_ls(a, v ^ [| d |]);

      // Proof:
      // - destruct_intros.
      // - peelr_induction sum_digits_positive_0 sum_digits_positive_S
      lemma sum_digits_positive: ∀ ℤ a, \list<ℤ> v;
        0 ≤ a ∧ vector_ge0(v) ⇒ 0 ≤ sum_digits_ms_to_ls(a, v);
    } */

#endif
